the_es:event_system{i:l}, j:es-E(the_es).
((es-first(the_es; j)))  es-causl(the_es; es-pred(the_es; j); j) 

latex

Definitions	x:A. B(x), P  Q, t  T, P  Q, prop{i:l}
Lemmas	es-axioms, es-pred wf, es-pred-locl, not wf, assert wf, es-first wf, es-E wf, event system wf